Nuprl Lemma : l_contains_wf
0,22
postcript
pdf
T
:Type,
A
,
B
:
T
List. l_contains(
T
;
A
;
B
)
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
x
.
t
(
x
)
,
x
L
.
P
(
x
)
,
l_contains(
T
;
A
;
B
)
Lemmas
l
all
wf
,
l
member
wf
origin
T:Type, A, B:T List. l_contains(T;A;B) 
Prop T:Type, A, B:T List. l_contains(T;A;B) Prop Tx:A. B(x) l)
x. t(x)xL. P(x)